Sections-14.agda:5,7-12
Set₁ != Set
when checking that the expression ∙ Set has type Set
